(0) Obligation:
Clauses:
gopher(nil, nil).
gopher(X, cons(nil, T)) :- ','(no(empty(X)), ','(head(X, nil), tail(X, T))).
gopher(X, Y) :- ','(no(empty(X)), ','(head(X, H), ','(no(empty(H)), ','(head(H, U), ','(tail(H, V), ','(tail(X, W), gopher(cons(U, cons(V, W)), Y))))))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, X), X).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).
Query: gopher(g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
gopherA(.(.(X1, X2), X3), X4) :- gopherA(cons(X1, cons(X2, X3)), X4).
gopherA(.(.(X1, X2), X3), X4) :- gopherA(cons(X1, cons(X2, X3)), X4).
Clauses:
gophercA(nil, nil).
gophercA(.(nil, X1), cons(nil, X1)).
gophercA(.(.(X1, X2), X3), X4) :- gophercA(cons(X1, cons(X2, X3)), X4).
gophercA(.(.(X1, X2), X3), X4) :- gophercA(cons(X1, cons(X2, X3)), X4).
Afs:
gopherA(x1, x2) = gopherA(x1)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
gopherA_in: (b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
GOPHERA_IN_GA(.(.(X1, X2), X3), X4) → U1_GA(X1, X2, X3, X4, gopherA_in_ga(cons(X1, cons(X2, X3)), X4))
GOPHERA_IN_GA(.(.(X1, X2), X3), X4) → GOPHERA_IN_GA(cons(X1, cons(X2, X3)), X4)
R is empty.
The argument filtering Pi contains the following mapping:
gopherA_in_ga(
x1,
x2) =
gopherA_in_ga(
x1)
.(
x1,
x2) =
.(
x1,
x2)
cons(
x1,
x2) =
cons(
x1,
x2)
GOPHERA_IN_GA(
x1,
x2) =
GOPHERA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
GOPHERA_IN_GA(.(.(X1, X2), X3), X4) → U1_GA(X1, X2, X3, X4, gopherA_in_ga(cons(X1, cons(X2, X3)), X4))
GOPHERA_IN_GA(.(.(X1, X2), X3), X4) → GOPHERA_IN_GA(cons(X1, cons(X2, X3)), X4)
R is empty.
The argument filtering Pi contains the following mapping:
gopherA_in_ga(
x1,
x2) =
gopherA_in_ga(
x1)
.(
x1,
x2) =
.(
x1,
x2)
cons(
x1,
x2) =
cons(
x1,
x2)
GOPHERA_IN_GA(
x1,
x2) =
GOPHERA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 2 less nodes.
(6) TRUE